(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v7 Bool)
(declare-const v10 Bool)
(declare-const v16 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const i7 Int)
(declare-const i9 Int)
(declare-const r1 Real)
(declare-const v17 Bool)
(declare-const v18 Bool)
(assert (not (exists ((q3 Real) (q4 (Array Real (_ BitVec 10))) (q5 Real)) v10)))
(declare-const arr--7714695575537527022_-9217426950762535450-0 (Array Int (Array Real (_ BitVec 10))))
(declare-const v19 Bool)
(declare-const arr--4043936453019934438_1550882884059009059-0 (Array Real (Array (_ BitVec 10) (_ BitVec 7))))
(assert (or (forall ((q6 (Array Real (_ BitVec 10))) (q7 (Array Real (_ BitVec 10)))) v16) (exists ((q6 (Array Real (_ BitVec 10))) (q7 (Array Real (_ BitVec 10)))) (not (distinct q7 q7)))))
(push)
(declare-const v20 Bool)
(declare-const i16 Int)
(assert (exists ((q12 Bool) (q13 (Array Real (Array (_ BitVec 10) (_ BitVec 7)))) (q14 (_ BitVec 4))) (not (= #xd q14 #xd q14 #xd))))
(assert (or v19 v18 v17 v10 (bvsge #b0100101000 #b0100101000) v5 v10 (not v5) v7))
(declare-const arr--7714695575537527022_-3001274412075095485-0 (Array Int Bool))
(assert (exists ((q15 (Array Int Bool)) (q16 Real)) (=> (< r1 q16 (sin r1)) (distinct q15 q15 arr--7714695575537527022_-3001274412075095485-0 arr--7714695575537527022_-3001274412075095485-0 arr--7714695575537527022_-3001274412075095485-0))))
(declare-const v21 Bool)
(check-sat)
